[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification key-order-def
enrich
   branch
, 
   string-less

with
   

   
   
   
   predicates  . < . : key × key;
   
   variables  ino : nat;
   
   

   

   axioms inode-less :  ⊦ inodekey(ino) < key ↔ ino < key.ino ∨ ¬ key.inode? ∧ ino = key.ino;
          used for: s, ls;
          dentrykey-less
          :  ⊦ dentrykey(ino, str) < key ↔ ino < key.ino ∨ key.dentry? ∧ ino = key.ino ∧ str < key.name ∨ key.data? ∧ ino = key.ino;
          used for: s, ls;
          datakey-less :  ⊦ datakey(ino, n) < key ↔ ino < key.ino ∨ key.data? ∧ ino = key.ino ∧ n < key.part;
          used for: s, ls;

   

   
end enrich